Nuprl Lemma : detach_fun_wf
6,26
postcript
pdf
T
:Type,
A
:(
T
Prop). detach_fun(
T
;
A
)
Type
latex
Definitions
x
:
A
.
B
(
x
)
,
Prop
,
t
T
,
detach_fun(
T
;
A
)
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
Lemmas
bool
wf
,
iff
wf
,
squash
wf
,
assert
wf
origin
T:Type, A:(T
Prop). detach_fun(T;A) 
Type T:Type, A:(TProp). detach_fun(T;A) Type x:A. B(x) T
Q
Q Q